DROPS

Document

System Description

DOI: 10.4230/OASIcs.ICLP.2018.11

SMT-Based Answer Set Solver CMODELS(DIFF) (System Description)

Authors: Da Shen and Yuliya Lierler

Published in: OASIcs, Volume 64, Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018)

Abstract

Many answer set solvers utilize Satisfiability solvers for search. Satisfiability Modulo Theory solvers extend Satisfiability solvers. This paper presents the CMODELS(DIFF) system that uses Satisfiability Modulo Theory solvers to find answer sets of a logic program. Its theoretical foundation is based on Niemala's characterization of answer sets of a logic program via so called level rankings. The comparative experimental analysis demonstrates that CMODELS(DIFF) is a viable answer set solver.

Cite as

Da Shen and Yuliya Lierler. SMT-Based Answer Set Solver CMODELS(DIFF) (System Description). In Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018). Open Access Series in Informatics (OASIcs), Volume 64, pp. 11:1-11:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{shen_et_al:OASIcs.ICLP.2018.11,
  author =	{Shen, Da and Lierler, Yuliya},
  title =	{{SMT-Based Answer Set Solver CMODELS(DIFF)}},
  booktitle =	{Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018)},
  pages =	{11:1--11:15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-090-3},
  ISSN =	{2190-6807},
  year =	{2018},
  volume =	{64},
  editor =	{Dal Palu', Alessandro and Tarau, Paul and Saeedloei, Neda and Fodor, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ICLP.2018.11},
  URN =		{urn:nbn:de:0030-drops-98775},
  doi =		{10.4230/OASIcs.ICLP.2018.11},
  annote =	{Keywords: answer set programming, satisfiability modulo theories, constraint satisfaction processing}
}

Search Results

Documents authored by Shen, Da

SMT-Based Answer Set Solver CMODELS(DIFF) (System Description)

Abstract

Cite as

Thanks for your feedback!

Could not send message